function Time(time)
{
  this.time = time || [];
}

Time.prototype.toString =
	function ()
	{
		return this.time.toString();
	}

Time.prototype.equals =
	function (object)
	{
		if (this === object)
		{
			return true;
		}
		return this.time.equals(object.time);
	};
	
Time.prototype.hashCode =
  function ()
  {
    return this.time.hashCode();
  }

Time.prototype.tick =
	function (value, k)
	{
		var newTime = this.time.slice(0);
		newTime.push(value);
		if (newTime.length > k)
		{
			newTime.shift();
		}
		return new Time(newTime);
	};
	
function StoreValue(aval, fresh)
{
  assertDefinedNotNull(aval);
  assertDefinedNotNull(aval.join);
  assertDefinedNotNull(aval.equals); 
  assertDefinedNotNull(aval.compareTo); 
	this.aval = aval;
	this.fresh = (fresh === undefined) ? 1 : fresh;
}

StoreValue.aval =
	function (storeValue)
	{
		return storeValue.aval;
	}

StoreValue.prototype.equals =
	function (x)
	{
		if (this === x)
		{
			return true;
		}
		return this.aval.equals(x.aval);
	}

StoreValue.prototype.compareTo =
  function (x)
  {
    // TODO does freshness plays a role in subsumption? Current answer: no.
    return this.aval.compareTo(x.aval);
  }

StoreValue.prototype.toString =
	function ()
	{
		return this.aval.toString();
	}

StoreValue.prototype.update =
	function (aval)
	{
		if (this.fresh === 1)
		{
			return this.strongUpdate(aval);
		}
		return this.weakUpdate(aval);
	}
	
StoreValue.prototype.strongUpdate =
	function (aval)
	{
		return new StoreValue(aval, 1);
	}

StoreValue.prototype.weakUpdate =
	function (aval)
	{
		return new StoreValue(this.aval.join(aval), 2);
	}

StoreValue.prototype.join =
  function (x)
  {
    if (x === BOT)
    {
      return this;
    }
    return new StoreValue(this.aval.join(x.aval), Math.max(this.fresh, x.fresh));
  }
	
StoreValue.prototype.reset =
	function ()
	{
    return new StoreValue(BOT, 0);      
	}
	
function Store(map)
{
	this.map = map || new HashMap();
}

Store.prototype.equals =
	function (x)
	{
    return this.compareTo(x) === 0;
	}

Store.prototype.compareTo =
  function (x)
  {
    return Lattice.subsumeComparison(this, x);
  }
  
Store.prototype.subsumes =
  function (x)
  {
    var xentries = x.map.entries();
    for (var i = 0; i < xentries.length; i++)
    {
      var xentry = xentries[i];
      var address = xentry.key;
      var thisStoreValue = this.map.get(address);
      if (!thisStoreValue)
      {
        return false;
      }
      var xStoreValue = xentry.value;
      var c = xStoreValue.compareTo(thisStoreValue);
      if (c === undefined || c > 0)
      {
        return false;
      }
    }
    return true;
  }

Store.prototype.diff = // debug
  function (x)
  {
    var diff = [];
    var entries = this.map.entries();
    for (var i = 0; i < entries.length; i++)
    {
      var entry = entries[i];
      var address = entry.key;
      var value = entry.value;
      var xvalue = x.map.get(address);
      if (xvalue)
      {
        if (!value.equals(xvalue))
        {
//          else
//          {
            diff.push(address + ":\n\t" + value + " (" + value.fresh + ")\n\t" + xvalue + " (" + xvalue.fresh + ")");            
//          }
          if (value.aval.isBenv && xvalue.aval.isBenv)
          {
            diff.push(value.aval.diff(xvalue.aval))
          }
        }
      }
      else
      {
        diff.push(address + ":\n\t" + value + " (" + value.fresh + ")\n\t<undefined>");
      }
    }
    var xentries = x.map.entries();
    for (i = 0; i < xentries.length; i++)
    {
      xentry = xentries[i];
      address = xentry.key;
      xvalue = xentry.value;
      var value = this.map.get(address);
      if (!value)
      {
        diff.push(address + ":\n\t<undefined>\n\t" + xvalue + " (" + xvalue.fresh + ")");
      }
    }
    return diff.join("\n");
  }

Store.prototype.toString =
	function ()
	{
    var entries = this.map.entries();
		return "{" + entries.map(
			function (entry)
			{
				return entry.key + " =" + entry.value.fresh + "=> " + entry.value;
			}).join(",") + "}";
	}

Store.prototype.nice =
	function ()
	{
  var entries = this.map.entries();
		return "\n{\n" + entries.map(
			function (entry)
			{
				return entry.key + " =" + entry.value.fresh + "=> " + entry.value;
			}).join("\n") + "\n}";
	}

Store.prototype.lookupAval =
	function (address)
	{
		var value = this.map.get(address);
		if (value)
		{
			return value.aval;
		}
		throw new Error("Store.lookupAval: no abstract value for address " + address + "\n" + this.nice());
	};
	
Store.prototype.allocAval =
	function (address, aval, undef)
	{
    assertDefinedNotNull(address);
    assertTrue(aval === BOT /*|| aval instanceof JipdaValue */|| aval.isBenv, "need JipdaValue or Benv");
		var value = this.map.get(address);
		if (value && value.fresh !== 0)
		{
		  var weaklyUpdatedValue = value.weakUpdate(aval);
//			print("REALLOCATED", address, weaklyUpdatedValue, msg ? msg : "", "-- was", entry);
		  var store = new Store(this.map.put(address, weaklyUpdatedValue)); 
		  store.weak = true; // hackety hack?
			return store;
		}
		var newValue = new StoreValue(aval);
//    print("ALLOCATED", address, newValue, msg ? msg : "", "-- was", entry);
		return new Store(this.map.put(address, newValue));
	};
	
Store.prototype.updateAval =
	function (address, aval, msg)
	{
    assertTrue((aval instanceof JipdaValue) || aval.isBenv, "need JipdaValue or Benv");
    var value = this.map.get(address);
		if (value)
		{
		  var updatedValue = value.update(aval);
//      print("UPDATED", address, updatedValue, msg ? msg : "", "-- was", entry);
			return new Store(this.map.put(address, updatedValue));
		}
		throw new Error("Store.updateAval: no abstract value at address " + address);
	};
	
Store.prototype.join =
  function (store)
  {
    if (store === BOT)
    {
      return this;
    }
    var result = new HashMap();
    var addresses = this.map.keys().concat(store.map.keys()).toSet();
    addresses.forEach(
      function (address)
      {
        var thisValue = this.map.get(address) || BOT;
        var otherValue = store.map.get(address) || BOT;
        var joinedValue = thisValue.join(otherValue);
        result = result.put(address, joinedValue);
      }, this);
    return new Store(result);
  }

Store.prototype.narrow =
	function (addresses)
	{
		var result = new HashMap();
		var entries = this.map.entries();
		for (var i = 0; i < entries.length; i++)
		{
		  var entry = entries[i];
      var address = entry.key;
      if (addresses.memberAt(address) > -1)
      {
        result = result.put(address, entry.value);
      }
//      if (address instanceof Addr)
//      {
//        var reset = entry[1].reset();
//        print("reset address", address, "before", entry[1], "after", reset);
//        return [[address, reset]];
//      }
		}
		return new Store(result);
	}

//Store.prototype.addresses =
//  function ()
//  {
//    return this.entries.entryKeys();
//  }
	
function Cont(name, node, index, benva, proc, marks, handler)
{
  this.name = name;
  this.node = node;
  this.index = index;
	this.benva = benva;
	this.proc = proc;
	this.marks = marks || [];
	this.handler = handler;
}

Cont.prototype.equals =
  function (other)
  {
    return this.node === other.node
      && this.name === other.name
      && this.index === other.index
      && this.benva.equals(other.benva)
//      && this.applications.setEquals(other.applications)  TODO review this, esp. for 'visited'
//      && Eq.equals(this.handler, other.handler)
  }

Cont.prototype.toString =
	function ()
	{
		return this.name + "-" + this.node.tag + (this.index ? ("-" + this.index) : "");
	};

Cont.prototype.execute =
	function (stack, store, time, c)
	{
//		print("---->", this, stack);
		// TODO remove (or rewrite) these asserts
    if (!(store instanceof Store))
    {
      throw new Error("no or wrong store:" + store);
    }
    if (!(time instanceof Time))
    {
      throw new Error("no or wrong time:" + time);
    }
    if (!c)
    {
      throw new Error("no or wrong c:" + c);
    }
		return this.proc(stack, store, time, c);
		// or, if cont execution in context of evaluator:
    // return this.proc.call(c.e, stack, store, time, c);
	};
	
Cont.prototype.addMark =
  function (mark)
  {
    var newMarks = this.marks.remove(mark).addFirst(mark);
//    print("ADDING", application, "OLD", this.applications, "NEW", newApplications);
    var cont = new Cont(this.name, this.node, this.index, this.benva, this.proc, newMarks, this.handler, this.props);
    return cont;
  };
	
	
Cont.prototype.setHandler =
  function (handler)
  {
    var cont = new Cont(this.name, this.node, this.index, this.benva, this.proc, this.marks, handler);
    return cont;
  }

function CallMark(application, funAddr, callable)
{
  this.application = application;
  this.funAddr = funAddr;
  this.callable = callable;
}
CallMark.prototype.equals = function (x) {return Eq.equals(this.application, x.application) && Eq.equals(this.funAddr, x.funAddr) && Eq.equals(this.callable, x.callable)}
CallMark.prototype.toString = function () {return "(" + this.application.tag + ", " + this.funAddr + ", " + this.callable + ")"};
		
function Task(msg, proc)
{
  this.msg = msg;
	this.proc = proc;
}

Task.prototype.toString =
  function ()
  {
    return this.msg;
  }

Task.prototype.execute =
	function ()
	{
		return this.proc();
	};


function gc(store, stack, benva)//, tasks)
{
  
	function benvReachable(benv, reachable)
	{	
		if (benv.isFunction())
		{
		  benv.Call.forEach(
		    function (Call) 
		    {
		      reachable = addressesReachable(Call.addresses(), reachable);		      		        
		    });
		}
		if (benv.isObject())
		{
			reachable = valueReachable(benv.Prototype, reachable);
		}
//		if (benv.parents)
//		{
		  reachable = addressesReachable(benv.parents, reachable);
//		}
		return addressesReachable(benv.addresses(), reachable);
	}
	
	function contReachable(cont, reachable)
	{
		return addressReachable(cont.benva, reachable);
	}
	
	function valueReachable(value, reachable)
	{
		if (value instanceof JipdaValue)
		{
			return addressesReachable(value.addresses(), reachable);
		}
    if (value instanceof Addr) // object pointer (currently only used for 'this' pointer in apply?)
    {
      return addressReachable(value, reachable);
    }
    if (value.isBenv) // object, env, ...
    {
      return benvReachable(value, reachable);
    }
		if (value instanceof Cont)
		{
			return contReachable(value, reachable);
		}
		if (Array.isArray(value))
		{
			return valuesReachable(value, reachable);
		}
		return reachable; // TODO investigate: when is getting here ok?
	}
	
	function valuesReachable(values, reachable)
	{
		for (var i = 0; i < values.length; i++)
		{
			reachable = valueReachable(values[i], reachable);
		}
		return reachable;
	}
	
	function addressReachable(address, reachable)
	{
		if (address === null)
		{
			return reachable;
		}
		if (reachable.memberAt(address) > -1)
		{
			return reachable;
		}
//		if (address instanceof Addr)
//		{
			var aval = store.lookupAval(address);
			assertDefinedNotNull(aval);
			return valueReachable(aval, reachable.addLast(address));
//		}
//		throw new Error("gc.addressReachable: cannot handle address " + address);
	}
	
	function addressesReachable(addresses, reachable)
	{
		for (var i = 0; i < addresses.length; i++)
		{
			reachable = addressReachable(addresses[i], reachable);
		}
		return reachable;
	}
	
//	function taskReachable(task, reachable)
//	{
//    //return addressReachable(task.benva, valuesReachable(task.stack, reachable));
//	  return reachable; 
//	}
	
//	function tasksReachable(tasks, reachable)
//	{
//		for (var i = 0; i < tasks.length; i++)
//		{
//			reachable = taskReachable(tasks[i], reachable);
//		}
//		return reachable;
//	}
	
//	print("GC", stack, benva, "\n", store);
//  var reachable = tasksReachable(tasks, addressReachable(benva, valuesReachable(stack, [])));
  var reachable = addressReachable(benva, valuesReachable(stack, []));
//	print("reachable", reachable);
  var narrowed = store.narrow(reachable);
	return narrowed;
}


function JipdaLattice(userLattice)
{
  assertDefinedNotNull(userLattice);
  this.userLattice = userLattice; 
  this.J_UNINITIALIZED = new JipdaValue(BOT, []);
  this.J_UNDEFINED = this.abst1(undefined);
  this.J_NULL = this.abst1(null);
  this.J_0 = this.abst1(0);
  this.J_1 = this.abst1(1);
  this.J_MININFINITY = this.abst1(-Infinity);
  this.U_0 = userLattice.abst1(0);
  this.U_1 = userLattice.abst1(1);
  this.U_TRUE = userLattice.abst1(true);
  this.U_FALSE = userLattice.abst1(false);
  this.U_THIS = userLattice.abst1("this");
  this.U_PROTOTYPE = userLattice.abst1("prototype");
  this.U_LENGTH = userLattice.abst1("length");
  this.U_NULL = userLattice.abst1(null);
}
JipdaLattice.prototype = new Lattice();

JipdaLattice.prototype.toString =
  function ()
  {
    return "[JipdaLattice (" + this.userLattice + ")]";
  }

JipdaLattice.prototype.abst =
  function (cvalues)
  {
    return cvalues.map(JipdaLattice.prototype.abst1, this).reduce(Lattice.join);
  }

JipdaLattice.prototype.abst1 =
  function (cvalue)
  {
    if (cvalue instanceof Addr)
    {
      return new JipdaValue(BOT, [cvalue]);
    }
    return new JipdaValue(this.userLattice.abst1(cvalue), []);
  }

JipdaLattice.prototype.isFalse =
  function (value)
  {
//    if (this.c.l.userLattice.isFalse(value.user)) // TODO move isTrue/isFalse to LatticeValue
//    {
//      return value.as.length === 0;
//    }
//    return false;
    throw new Error();
  }

JipdaLattice.prototype.isTrue =
  function (value)
  {
//    return this.c.l.userLattice.isTrue(value.user)) // TODO move isTrue/isFalse to LatticeValue
    throw new Error(); // use ToBoolean first, then use isTrue/False on user value
  }

function JipdaValue(user, as)
{
  assertDefinedNotNull(user);
  assertDefinedNotNull(as);
  this.user = user;
  this.as = as;
}
JipdaValue.prototype = new LatticeValue();

JipdaValue.prototype.accept =
  function (visitor)
  {
    return visitor.visitJipdaValue(this);
  }

JipdaValue.prototype.addresses =
  function ()
  {
    return this.as.slice(0);
  }

JipdaValue.prototype.isAddress =
  function ()
  {
    return this.user === BOT;
  }

JipdaValue.prototype.toString =
  function (printer)
  {
    return "[" + this.user.toString(printer) + ", " + (printer ? this.as.map(printer) : this.as) + "]";
  }

JipdaValue.prototype.join =
  function (x)
  {
    if (x === BOT)
    {
      return this;
    }
    return new JipdaValue(this.user.join(x.user), this.as.concat(x.as).toSet());
  }

JipdaValue.prototype.compareTo =
  function (x)
  {
    if (x === BOT)
    {
      return 1;
    }
    
    if (x === this)
    {
      return 0;
    }

    var c1 = this.user.compareTo(x.user);
    if (c1 === undefined)
    {
      return undefined;
    }
    var c2 = Lattice.subsumeComparison(this.as, x.as);
    return Lattice.joinCompareResults(c1, c2);
  }

// TODO move this into JipdaValue as methods (and have JV NOT inherit from LatticeValue)

function toUserString(j, store)
{
  var objs = j.as.map(Store.prototype.lookupAval, store);
  // 8.12.8 The [...] specification of [[DefaultValue]] for native objects can return only primitive values.
  // !!! DefaultValue must return user value
  var vals = objs.map(function (o) {return o.DefaultValue("string")});
  var u = j.user.join(vals.reduce(Lattice.join, BOT)).ToString();
  return u;
}  

function toUserNumber(j, store)
{
  var objs = j.as.map(Store.prototype.lookupAval, store);
  var vals = objs.map(function (o) {return o.DefaultValue("number")});
  var u = j.user.join(vals.reduce(Lattice.join, BOT)).ToNumber();
  return u;
}  

function toUserInt32(j, store)
{
  var objs = j.as.map(Store.prototype.lookupAval, store);
  var vals = objs.map(function (o) {return o.DefaultValue("number")});
  var r = j.user.join(vals.reduce(Lattice.join, BOT));
//  if (!r.ToInt32) print("HELP", r, r.constructor);
  var u = j.user.join(vals.reduce(Lattice.join, BOT)).ToInt32();
  return u;
}  

function toUserBoolean(j) // no store: objects are 'true' (no need for lookup)
{
  return j.user.ToBoolean().join(j.as.length === 0 ? BOT : c.l.userLattice.abst1(true));
}


//// ToBoolean
//// ToString
//// ToUint32


function Jipda(config)
{
  // start constants
  var performGc = config.gc === undefined ? true : config.gc;
  var k = config.k === undefined ? 1 : config.k;
  var userLattice = config.lattice;
  var lattice = new JipdaLattice(userLattice);
  var ag = config.ag;
  var visited = config.visited || new DefaultVisitedStrategy(performGc ? gc : function (store) {return store}); // TODO make this mandatory param
  var benvFactory = config.benv || new DefaultBenv();
  var evaluator = config.evaluator || jseval;
  
  assertDefinedNotNull(k);
  assertDefinedNotNull(userLattice);
  assertDefinedNotNull(ag);
  assertDefinedNotNull(visited);
  
  // end constants
	
  function createEnvironment(parenta, sourceNode, declarationNode, c)
  {
    var benv = benvFactory.createEnvironment(parenta, sourceNode, declarationNode);
    return {benv:benv};
  }

  function createObject(Prototype)
  {
    assertDefinedNotNull(Prototype, "[[Prototype]]");
    var benv = benvFactory.createObject(Prototype);
    return benv;
  }

  function createArray()
  {
    var benv = benvFactory.createArray(ARRAYPA);
    return benv;
  }

  function createString(prim)
  {
    assertDefinedNotNull(prim, "prim");
    var benv = benvFactory.createString(prim, STRINGPA);
    return benv;
  }

  function createClosure(node, scope)
  {
    var benv = benvFactory.createFunction(new BenvClosureCall(node, scope), FUNCTIONPA);
    return benv;
  }

  function createPrimitive(applyFunction)
  {
    var benv = benvFactory.createFunction(new BenvPrimitiveCall(applyFunction), FUNCTIONPA);
    return benv;
  }
	    
  
  // 9.3
  function ToNumber(value, node, stack, benva, store, time, c)
  {
    
    if (value.addresses().length === 0)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      return cont.execute(stack2.addFirst(new JipdaValue(value.user.ToNumber(), [])), store, time, c);
    }
    
    var tasks = DefaultValue(value.addresses(), function (primValue) {return primValue.ToNumber()}, node, stack, benva, store, time, c); 
    if (value.user === BOT)
    {
      return tasks;
    }
    
    return tasks.addFirst(
      new Task("primitive part ToNumber",
        function ()
        {
          var cont = stack[0];
          var stack2 = stack.slice(1);
          return cont.execute(stack2.addFirst(new JipdaValue(value.user.ToNumber(), [])), store, time, c);
        }));
  }
  
  // 9.6
  function ToUInt32(value, node, stack, benva, store, time, c)
  {
    
    if (value.addresses().length === 0)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      return cont.execute(stack2.addFirst(new JipdaValue(value.user.ToUInt32(), [])), store, time, c);
    }
    
    var tasks = DefaultValue(value.addresses(), function (primValue) {return primValue.ToUInt32()}, node, stack, benva, store, time, c); 
    if (value.user === BOT)
    {
      return tasks;
    }
    
    return tasks.addFirst(
      new Task("primitive part ToNumber",
        function ()
        {
          var cont = stack[0];
          var stack2 = stack.slice(1);
          return cont.execute(stack2.addFirst(new JipdaValue(value.user.ToUInt32(), [])), store, time, c);
        }));
  }
  
  
  // 9.8
  function ToString(value, node, stack, benva, store, time, c)
  {
    
    if (value.addresses().length === 0)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      return cont.execute(stack2.addFirst(new JipdaValue(value.user.ToString(), [])), store, time, c);
    }
    
    var tasks = DefaultValueString(value.addresses(), node, function (primValue) {return primValue.ToString()}, stack, benva, store, time, c); 
    if (value.user === BOT)
    {
      return tasks;
    }
    
    return tasks.addFirst(
      new Task("primitive part ToString",
        function ()
        {
          var cont = stack[0];
          var stack2 = stack.slice(1);
          return cont.execute(stack2.addFirst(new JipdaValue(value.user.ToString(), [])), store, time, c);
        }));
  }
  
  function stackElementsSubsume(s1, s2)
  {
    if (s1.length < s2.length)
    {
      return false;
    }
    return true;
  }
  					
  function BenvPrimitiveCall(applyFunction)
  {
    this.applyFunction = applyFunction;
  }

  BenvPrimitiveCall.prototype.toString =
    function ()
    {
      return "<BenvPrimitiveCall>";
    }
  
  BenvPrimitiveCall.prototype.equals =
    function (other)
    {
      if (this === other)
      {
        return true;
      }
      if (!(this instanceof BenvPrimitiveCall))
      {
        return false;
      }
      return this.applyFunction === other.applyFunction; // this case needed? (finite number of fixed prims)
    }
  
  BenvPrimitiveCall.prototype.mark =
    function (cont, application, funAddr)
    {
      var markedCont = cont.addMark(new CallMark(application, funAddr, this));
      markedCont.toString = cont.toString; // DEBUG
      return markedCont;
    }

  BenvPrimitiveCall.prototype.addresses =
    function ()
    {
      return [];
    } 
  
	
	var totalNumTasks = 0;
	
	function taskRunner(tasks)
	{
		while (tasks.length > 0)
		{
      if (tasks.length > 512)
      {
        throw new Error("task overflow");
      }
      if (totalNumTasks > 1024)
      {
        throw new Error("state space overflow");
      }
		  var task = tasks[0];
//		  print("\nSTART", task, "-- length", tasks.length);
			var taskResult = task.execute();
			assertDefinedNotNull(taskResult);
//			print("END", task, "-- result", taskResult)//, "-- total", ++totalNumTasks);
			tasks = tasks.slice(1).concat(taskResult);
		}		
	}

	
	var globala = new ContextAddr("this", 0);
  var GLOBALA = lattice.abst1(globala); // global this
  var OBJECTPA; // Object.prototype
  var FUNCTIONPA; // Function.prototype
  var STRINGPA; // String.prototype
  var ARRAYPA; // Array.prototype
  
  function createGlobal(store)
  {
    
    function registerProperty(object, propertyName, value)
    {
      object = object.add(userLattice.abst1(propertyName), value);
      return object;      
    }

    function registerPrimitiveFunction(object, objectAddress, propertyName, fun)
    {
      var primFunObject = createPrimitive(fun);
      var primFunObjectAddress = new ContextAddr(objectAddress, "<" + propertyName + ">"); 
      store = store.allocAval(primFunObjectAddress, primFunObject);    
      return registerProperty(object, propertyName, lattice.abst1(primFunObjectAddress));
    }
    
    // BEGIN PROTOTYPES
    // first we need to establish 'global' and some prototypes,
    // because for example: 'createPrimitive' relies on 'FUNCTIONPA', 'FUNCTIONPA' relies on OBJECTPA
    
    var objectPa = new ContextAddr("Object.prototype", 0);
    OBJECTPA = lattice.abst1(objectPa);
    var objectP = createObject(lattice.J_NULL);
    objectP.toString = function () { return "<Object.prototype>"; }; // debug

    var functionPa = new ContextAddr("Function.prototype", 0);
    FUNCTIONPA = lattice.abst1(functionPa);
    var functionP = createObject(OBJECTPA);
    functionP.toString = function () { return "<Function.prototype>"; }; // debug

    var stringPa = new ContextAddr("String.prototype", 0);
    STRINGPA = lattice.abst1(stringPa);
    var stringP = createObject(OBJECTPA);
    stringP.toString = function () { return "<String.prototype>"; }; // debug

    var arrayPa = new ContextAddr("Array.prototype", 0);
    ARRAYPA = lattice.abst1(arrayPa);
    var arrayP = createObject(OBJECTPA);
    arrayP.toString = function () { return "<Array.prototype>"; }; // debug
    
    var global = createObject(OBJECTPA);
    // END PROTOTYPES
    
    // BEGIN OBJECT
    var objecta = new ContextAddr("<Object>", 0);
    objectP = registerProperty(objectP, "constructor", lattice.abst1(objecta));
    
    var object = createPrimitive(objectConstructor);
    object = object.add(lattice.U_PROTOTYPE, OBJECTPA);//was OBJECTPA
    global = global.add(userLattice.abst1("Object"), lattice.abst1(objecta));
    
    object = registerPrimitiveFunction(object, objecta, "getPrototypeOf", objectGetPrototypeOf);
    object = registerPrimitiveFunction(object, objecta, "create", objectCreate);

    store = store.allocAval(objecta, object);
    store = store.allocAval(objectPa, objectP);
    // END OBJECT

        
    // BEGIN FUNCTION
    var functiona = new ContextAddr("<Function>", 0);
    var functionP = registerProperty(functionP, "constructor", lattice.abst1(functiona));
    var fun = createPrimitive(function () {}); // TODO
    fun = fun.add(lattice.U_PROTOTYPE, FUNCTIONPA);
    global = global.add(userLattice.abst1("Function"), lattice.abst1(functiona));
    store = store.allocAval(functiona, fun);

    store = store.allocAval(functionPa, functionP);
    // END FUNCTION 
            
    // BEGIN STRING
    var stringa = new ContextAddr("<String>", 0);
    var stringP = registerProperty(stringP, "constructor", lattice.abst1(stringa));
    var string = createPrimitive(stringConstructor);
    string = string.add(lattice.U_PROTOTYPE, STRINGPA);
    var stringNa = new ContextAddr("String", 0);
    global = global.add(userLattice.abst1("String"), lattice.abst1(stringa));
    store = store.allocAval(stringa, string);

    store = store.allocAval(stringPa, stringP);
    // END STRING 
            
    // BEGIN ARRAY
    var arraya = new ContextAddr("<Array>", 0);
    var arrayP = registerProperty(arrayP, "constructor", lattice.abst1(arraya));
    var array = createPrimitive(arrayConstructor);
    array = array.add(lattice.U_PROTOTYPE, ARRAYPA);
    var arrayNa = new ContextAddr("Array", 0);
    store = store.allocAval(arraya, array);
    global = global.add(userLattice.abst1("Array"), lattice.abst1(arraya));
    
    arrayP = registerPrimitiveFunction(arrayP, arrayPa, "concat", arrayConcat);
    arrayP = registerPrimitiveFunction(arrayP, arrayPa, "push", arrayPush);
    arrayP = registerPrimitiveFunction(arrayP, arrayPa, "map", arrayMap);
    arrayP = registerPrimitiveFunction(arrayP, arrayPa, "reduce", arrayReduce); // TODO
    arrayP = registerPrimitiveFunction(arrayP, arrayPa, "filter", arrayFilter);
    store = store.allocAval(arrayPa, arrayP);
    // END ARRAY
    
    
    // BEGIN MATH
    var math = createObject(OBJECTPA);
    math = registerPrimitiveFunction(math, globala, "abs", mathAbs);
    math = registerPrimitiveFunction(math, globala, "round", mathRound);
    math = registerPrimitiveFunction(math, globala, "sin", mathCos);
    math = registerPrimitiveFunction(math, globala, "cos", mathSin);
    math = registerPrimitiveFunction(math, globala, "sqrt", mathSqrt);
    math = registerPrimitiveFunction(math, globala, "max", mathMax);
    math = registerPrimitiveFunction(math, globala, "random", mathRandom);
    math = registerProperty(math, "PI", lattice.abst1(Math.PI));
    var matha = new ContextAddr("<Math>", 0);
    store = store.allocAval(matha, math);
    global = global.add(userLattice.abst1("Math"), lattice.abst1(matha));
    // END MATH
    
    // BEGIN GLOBAL
    global = global.add(lattice.U_THIS, GLOBALA); // global "this" address
    
    // ECMA 15.1.1 value properties of the global object (no "null", ...)
    global = registerProperty(global, "undefined", lattice.J_UNDEFINED);
    global = registerProperty(global, "NaN", lattice.abst1(NaN));
    global = registerProperty(global, "Infinity", lattice.abst1(Infinity));

    // specific interpreter functions
    global = registerPrimitiveFunction(global, globala, "$meta", $meta);
    global = registerPrimitiveFunction(global, globala, "$join", $join);
    global = registerPrimitiveFunction(global, globala, "print", _print);
    // end specific interpreter functions
    
    store = store.allocAval(globala, global);
    // END GLOBAL
    
    // BEGIN PRIMITIVES
    function objectConstructor(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var obj = createObject(OBJECTPA);
      store = c.e.allocAval(objectAddress, obj, stack, store, c);
      return cont.execute(stack2.addFirst(c.l.abst1(objectAddress)), store, time, c);
    }    
    
    function objectCreate(application, operands, objectAddress, stack, benva, store, time, c)
    {
      if (operands.length !== 1)
      {
        throw new Error("TODO");
      }
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var obj = createObject(operands[0]);
      var address = ag.object(application, time);
      store = c.e.allocAval(address, obj, stack, store, c);
      return cont.execute(stack2.addFirst(c.l.abst1(address)), store, time, c);
    }    
    
    function objectGetPrototypeOf(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var operand = operands[0];
      if (operand.user === BOT)
      {
        var addresses = operand.addresses();
        var object = addresses.map(store.lookupAval, store).reduce(Lattice.join);
        return cont.execute(stack2.addFirst(object.Prototype), store, time, c);
      }
      throw new Error("TODO");
    }    

    function stringConstructor(application, operands, ths, stack, benva, store, time, c)
    {
      // TODO (also for other built-in constructors): throwing away freshly created object (that has different addr, so not that bad)!
      // (postpone creating fresh object?)
      if (isNewExpression(application))
      {
        var cont = stack[0];
        var stack2 = stack.slice(1);

        if (operands.length === 0)
        {
          var stringBenv = c.createString(c.l.userLattice.abst1("")); // TODO constant 
          var stringAddress = ag.string(application, time);
          stringBenv = stringBenv.add(lattice.U_LENGTH, c.l.J_0);
          store = c.e.allocAval(stringAddress, stringBenv, stack, store);
          return cont.execute(stack2.addFirst(c.l.abst1(stringAddress)), store, time, c);
        }
        
        var prim = operands[0].user.ToString(); // TODO ToString iso. project
        var stringBenv = c.createString(prim); 
        var stringAddress = ag.array(application, time); // TODO this is not an array(!)
        stringBenv = stringBenv.add(lattice.U_LENGTH, new JipdaValue(prim.length(), []));
        store = c.e.allocAval(stringAddress, stringBenv, stack, store);
        return cont.execute(stack2.addFirst(c.l.abst1(stringAddress)), store, time, c);        
      }
      if (operands.length === 0)
      {
        var cont = stack[0];
        var stack2 = stack.slice(1);
        return cont.execute(stack2.addFirst(c.l.abst1("")), store, time, c); // TODO constant  
      }
      return c.e.ToString(application, stack.addFirst(operands[0]), benva, store, time, c);
    }    
        
    function arrayConstructor(application, operands, ths, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var arrayBenv = createArray();
      var arrayAddress = ag.array(application, time);
      var l;
      if (operands.length === 0)
      {
        l = lattice.J_0;
      }
      else
      {
        l = operands[0];
      }
      arrayBenv = arrayBenv.add(lattice.U_LENGTH, l);
      store = c.e.allocAval(arrayAddress, arrayBenv, stack, store);
      return cont.execute(stack2.addFirst(c.l.abst1(arrayAddress)), store, time, c);
    }    
    
    function arrayPush(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
     
      var arg0aa = operands[0];
                    
      var receiver = c.e.lookupAval(objectAddress, stack, store, c);
      var lreceiver = receiver.lookup(c.l.U_LENGTH).value;
      if (lreceiver === BOT)
      {
        // this branch is untested (need apply or call)
//        receiver = receiver.add(lattice.U_0.ToString(), newPropertyAddress);
//        store = c.e.allocAval(newPropertyAddress, arg0aa, stack, store, c);
//        var lengthPropertyAddress = ag.objectPropery(objectAddress, c.l.U_LENGTH);
//        receiver = receiver.add(lattice.U_LENGTH, lengthPropertyAddress);
//        store = c.e.allocAval(lengthPropertyAddress, c.l.J_0, stack, store, c);
//        store = c.e.sideEffectAval(objectAddress, receiver, stack, store, c);
//        return cont.execute(stack2.addFirst(arg0aa), store, time, c);
        throw new Error("TODO");
      }
      else
      {
        var lreceiveru = lreceiver.user;
        receiver = receiver.add(lreceiveru.ToString(), arg0aa);
        var newLengthu = c.l.userLattice.add(lreceiveru, c.l.U_1);
        var newLength = new JipdaValue(newLengthu, []);
        receiver = receiver.add(c.l.U_LENGTH, newLength);
        store = c.e.sideEffectAval(objectAddress, receiver, stack, store, c);
        return cont.execute(stack2.addFirst(newLength), store, time, c);                                                                                  
      }
    }
    
    function arrayConcat(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
     
      var arg0aa = operands[0];

      var receiver = c.e.lookupAval(objectAddress, stack, store, c);
      var lreceiveru = receiver.lookup(c.l.U_LENGTH).value.user;
      var arg0 = c.e.doLookupAddresses(arg0aa.addresses(), stack, store, c);
      var larg0 = arg0.lookup(c.l.U_LENGTH).value;
      var larg0u = larg0.user;
      var result = c.createArray();
      var resulta = c.a.array(application, time);
      return arrayCopy(receiver, c.l.U_0, result, c.l.U_0, lreceiveru, stack, store, c,
        function (result, index, store, c)
        {
          return arrayCopy(arg0, lattice.U_0, result, index, larg0u, stack, store, c, 
            function (result, index, store, c)
            {
              result = result.add(c.l.U_LENGTH, new JipdaValue(index, []));
              store = c.e.allocAval(resulta, result, stack, store, c);
              return cont.execute(stack2.addFirst(c.l.abst1(resulta)), store, time, c);                                                                                  
            });
        });
    } 
    
    function arrayMap(application, operands, thisa, stack, benva, store, time, c)
    {
      // TODO ToObject(thisa)
      // TODO best way to solve this?
      var receiver = c.e.lookupAval(thisa, stack, store, c);
      var lenValue = receiver.lookup(lattice.U_LENGTH).value;
      
      function arrayMapToUInt32Cont()
      {
        return new Cont("arrayMapToUInt32", application, null, benva,
          function (stack, store, time, c)
          {
            var lenPrim = stack[0].user;
            var stack2 = stack.slice(1);
            
            var arr = createArray();
            var arrAddr = ag.array(application, time);
            store = store.allocAval(arrAddr, arr, stack, store, c);
            
            
            function arrayMapLoop(k, arr, stack, store, time, c)
            {
              while (c.l.userLattice.isTrue(c.l.userLattice.lt(k, lenPrim)))
              {
                var indexValue = receiver.lookup(k.ToString()).value;
                if (indexValue !== BOT && !indexValue.equals(c.l.J_UNDEFINED)) // TODO project defined/undefined
                {
                  return c.e.applyProc(application, [c.l.abst1(thisa), new JipdaValue(k, []), indexValue, operands[0], operands[1] || c.GLOBALA, arrayMapCont(k, arr)].concat(stack), benva, store, time, c, 3); // TODO this addresses          
                }
                k = c.l.userLattice.add(k, lattice.U_1);
              }

              arr = arr.add(lattice.U_LENGTH, new JipdaValue(lenPrim, []));
              store = c.e.sideEffectAval(arrAddr, arr, stack, store, c);
              //stack[0] jarr    (GC)
              //stack[1] f       (GC)
              //stack[2] this    (GC)
              var cont = stack[3];
              var stack2 = stack.slice(4);
              return cont.execute(stack2.addFirst(jarr), store, time, c);            
            }
            
            function arrayMapCont(k, arr)
            {
              return new Cont("arrayMap", application, k, benva,
                function (stack, store, time, c)
                {
                  var value = stack[0];
                  var stack2 = stack.slice(1);
                  arr = arr.add(k.ToString(), value);
                  // side-effect now for GC
                  store = c.e.sideEffectAval(arrAddr, arr, stack, store, c);
                  return arrayMapLoop(c.l.userLattice.add(k, lattice.U_1), arr, stack2, store, time, c);
                });
            }
            
            var jarr = c.l.abst1(arrAddr);
            return arrayMapLoop(lattice.U_0, arr, stack2.addFirst(jarr), store, time, c);            
          });
      }
      
      // add thisAddr and fAddr to rootset 
      var stack2 = stack.addFirst(thisa).addFirst(operands[0]);
      return ToUInt32(lenValue, application, stack2.addFirst(arrayMapToUInt32Cont()), benva, store, time, c);
    }
    
    function arrayReduce(application, operands, thisa, stack, benva, store, time, c)
    {
      // TODO ToObject(thisa)
      // TODO best way to solve this?
      var receiver = c.e.lookupAval(thisa, stack, store, c);
      var lenValue = receiver.lookup(lattice.U_LENGTH).value;
      
      function arrayReduceToUInt32Cont()
      {
        return new Cont("arrayReduceToUInt32", application, null, benva,
          function (stack, store, time, c)
          {
            var lenPrim = stack[0].user;
            var k = lattice.U_0;
            if (operands[1])
            {
              return arrayReduceLoop(k, operands[1], stack, store, time, c);
            }
            else
            {
              if (c.l.userLattice.isTrue(c.l.userLattice.eqq(lenPrim, lattice.U_0)))
              {
                var stack2 = stack.slice(1);
                return performThrow(c.l.abst1("Type error"), application, stack2, benva, store, time, c);
              }
              while (c.l.userLattice.isTrue(c.l.userLattice.lt(k, lenPrim)))
              {
                var indexValue = receiver.lookup(k.ToString()).value;
                if (indexValue !== BOT)
                {
                  return arrayReduceLoop(c.l.userLattice.add(k, lattice.U_1), indexValue, stack, store, time, c);
                }
                k = c.l.userLattice.add(k, lattice.U_1);
              }              
            }
            
            function arrayReduceLoop(k, result, stack, store, time, c)
            {
              while (c.l.userLattice.isTrue(c.l.userLattice.lt(k, lenPrim)))
              {
                var indexValue = receiver.lookup(k.ToString()).value; // TODO here, and similar methods, proto lookup?
                if (indexValue !== BOT)
                {
                  var stack2 = stack.slice(1);
                  return c.e.applyProc(application, [c.l.abst1(thisa), new JipdaValue(k, []), indexValue, result, operands[0], c.l.abst1(thisa), arrayReduceCont(k)].concat(stack2), benva, store, time, c, 4); // TODO this addresses          
                }
                k = c.l.userLattice.add(k, lattice.U_1);
              }
              //stack[0] index value
              //stack[1] GC
              //stack[2] GC
              var cont = stack[3];
              var stack2 = stack.slice(4);
              return cont.execute(stack2.addFirst(result), store, time, c);            
            }
            
            function arrayReduceCont(k)
            {
              return new Cont("arrayReduce", application, k, benva,
                function (stack, store, time, c)
                {
                  var result = stack[0];
                  return arrayReduceLoop(c.l.userLattice.add(k, lattice.U_1), result, stack, store, time, c);
                });
            }
          });
      }
      
      // add receiver, reducer to rootset
      var stack2 = stack.addFirst(thisa).addFirst(operands[0]);
      return ToUInt32(lenValue, application, stack2.addFirst(arrayReduceToUInt32Cont()), benva, store, time, c);
    }

    function arrayFilter(application, operands, thisa, stack, benva, store, time, c)
    {
      // TODO ToObject(thisa)
      // TODO best way to solve this?
      var receiver = c.e.lookupAval(thisa, stack, store, c);
      var lenValue = receiver.lookup(lattice.U_LENGTH).value;
      
      function arrayFilterToUInt32Cont() // TODO numAllocedProperties is concrete integer (used as index), k is abstract???
      { // but numAP is also used to slice stuff of stack... make two counters: concrete and abst?
        // Points against: every JS conc value should be abstractable
        return new Cont("arrayFilterToUInt32", application, null, benva,
          function (stack, store, time, c)
          {
            var lenPrim = stack[0].user;
            var stack2 = stack.slice(1);
            
            var arr = createArray();
            var arrAddr = ag.array(application, time);
            var jarr = c.l.abst1(arrAddr);
            store = c.e.allocAval(arrAddr, arr, stack, store, c);
            
            function arrayFilterLoop(k, numAllocedProperties, arr, stack, store, time, c)
            {
              while (c.l.userLattice.isTrue(c.l.userLattice.lt(k, lenPrim)))
              {
                var indexValue = receiver.lookup(k.ToString()).value;
                if (indexValue !== BOT && !indexValue.equals(c.l.J_UNDEFINED)) // TODO project defined/undefined
                {
                  return c.e.applyProc(application, [indexValue, new JipdaValue(k, []), indexValue, operands[0], operands[1] || c.GLOBALA, arrayFilterCont(k, indexValue, numAllocedProperties, arr)].concat(stack), benva, store, time, c, 3); // TODO this addresses          
                }
                k = c.l.userLattice.add(k, c.l.U_1);
              }
              
              arr = arr.add(lattice.U_LENGTH, c.l.abst1(numAllocedProperties));
              store = c.e.sideEffectAval(arrAddr, arr, stack, store, c);
              //stack[0] jarr    (GC)
              //stack[1] f       (GC)
              //stack[2] this    (GC)
              var cont = stack[3];
              var stack2 = stack.slice(4);
              return cont.execute(stack2.addFirst(jarr), store, time, c);            
            }
            
            function arrayFilterCont(k, indexValue, numAllocedProperties, arr)
            {
              return new Cont("arrayFilter", application, k, benva,
                function (stack, store, time, c)
                {
                  var value = toUserBoolean(stack[0]);
                  var stack2 = stack.slice(1);
                  if (c.l.userLattice.isTrue(value))
                  {
                    var propName = c.l.userLattice.abst1(String(numAllocedProperties));
                    arr = arr.add(propName, indexValue);
                    // side-effect now for GC
                    store = c.e.sideEffectAval(arrAddr, arr, stack, store, c);
                    return arrayFilterLoop(c.l.userLattice.add(k, lattice.U_1), numAllocedProperties + 1, arr, stack2, store, time, c);                    
                  }
                  if (c.l.userLattice.isFalse(value))
                  {
                    return arrayFilterLoop(c.l.userLattice.add(k, lattice.U_1), numAllocedProperties, arr, stack2, store, time, c);
                  }
                  return [new Task("Array.prototype.filter true",
                            function ()
                            { // copied
                              var propName = c.l.userLattice.abst1(String(numAllocedProperties));
                              arr = arr.add(propName, indexValue);
                              // side-effect now for GC
                              store = c.e.sideEffectAval(arrAddr, arr, stack, store, c);
                              return arrayFilterLoop(c.l.userLattice.add(k, lattice.U_1), numAllocedProperties + 1, arr, stack2, store, time, c);                    
                            }),
                          new Task("Array.prototype.filter false",
                            function ()
                            { // copied
                              return arrayFilterLoop(c.l.userLattice.add(k, lattice.U_1), numAllocedProperties, arr, stack2, store, time, c);
                            })];
                });
            }
            return arrayFilterLoop(c.l.U_0, 0, arr, stack2.addFirst(jarr), store, time, c);            
          });
      }
      
      // add receiver, filter function to rootset
      var stack2 = stack.addFirst(thisa).addFirst(operands[0]);
      return ToUInt32(lenValue, application, stack2.addFirst(arrayFilterToUInt32Cont()), benva, store, time, c);
    }    
    
    function mathSqrt(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var u = toUserNumber(operands[0], store);
      var r = c.l.userLattice.sqrt(u);
      var j = new JipdaValue(r, []);
      return cont.execute(stack2.addFirst(j), store, time, c);
    }
    
    function mathAbs(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var u = toUserNumber(operands[0], store);
      var r = c.l.userLattice.abs(u);
      var j = new JipdaValue(r, []);
      return cont.execute(stack2.addFirst(j), store, time, c);
    }
    
    function mathRound(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var u = toUserNumber(operands[0], store);
      var r = c.l.userLattice.round(u);
      var j = new JipdaValue(r, []);
      return cont.execute(stack2.addFirst(j), store, time, c);
    }
    
    function mathSin(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var u = toUserNumber(operands[0], store);
      var r = c.l.userLattice.sin(u);
      var j = new JipdaValue(r, []);
      return cont.execute(stack2.addFirst(j), store, time, c);
    }
    
    function mathCos(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var u = toUserNumber(operands[0], store);
      var r = c.l.userLattice.cos(u);
      var j = new JipdaValue(r, []);
      return cont.execute(stack2.addFirst(j), store, time, c);
    }
    
    function mathMax(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      if (operands.length === 2)
      {
        var u1 = toUserNumber(operands[0], store);
        var u2 = toUserNumber(operands[1], store);
        var r = c.l.userLattice.max(u1, u2);
        var j = new JipdaValue(r, []);
        return cont.execute(stack2.addFirst(j), store, time, c);        
      }
      throw new Error("NYI");
    }
    
    // deterministic random from Octane benchmarks 
    var seed = 49734321;
    function mathRandom(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      // Robert Jenkins' 32 bit integer hash function.
      seed = ((seed + 0x7ed55d16) + (seed << 12))  & 0xffffffff;
      seed = ((seed ^ 0xc761c23c) ^ (seed >>> 19)) & 0xffffffff;
      seed = ((seed + 0x165667b1) + (seed << 5))   & 0xffffffff;
      seed = ((seed + 0xd3a2646c) ^ (seed << 9))   & 0xffffffff;
      seed = ((seed + 0xfd7046c5) + (seed << 3))   & 0xffffffff;
      seed = ((seed ^ 0xb55a4f09) ^ (seed >>> 16)) & 0xffffffff;
      var r = c.l.userLattice.abst1((seed & 0xfffffff) / 0x10000000);
      var j = new JipdaValue(r, []);
      return cont.execute(stack2.addFirst(j), store, time, c);
    }
    
    function $meta(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var str = operands[0].conc()[0];
      var value = c.l.abst1(eval(str));
      return cont.execute(stack2.addFirst(value), store, time, c);
    }
    
    function $join(application, operands, thisa, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var value = operands.reduce(Lattice.join, BOT);
      return cont.execute(stack2.addFirst(value), store, time, c);
    }    
    
    function $toString(application, operands, thisa, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      var value = operands.reduce(Lattice.join, BOT);
      return cont.execute(stack2.addFirst(value), store, time, c);
    }    
    
    function _print(application, operands, objectAddress, stack, benva, store, time, c)
    {
      var cont = stack[0];
      var stack2 = stack.slice(1);
      print.apply(null, operands);
      return cont.execute(stack2.addFirst(lattice.J_UNDEFINED), store, time, c);
    }    
    // END PRIMITIVES
    
    // BEGIN HELPERS
    function arrayCopy(srcBenv, srcPos, dstBenv, dstPos, l, stack, store, c, fcont)
    {
      var i = c.l.U_0;
      while (c.l.userLattice.isTrue(c.l.userLattice.lt(i, l)))
      {
        var srcvalue = srcBenv.lookup(c.l.userLattice.add(i, srcPos).ToString()).value;
        var dstName = c.l.userLattice.add(i, dstPos).ToString();
        dstBenv = dstBenv.add(dstName, srcvalue);
        i = c.l.userLattice.add(i, c.l.U_1);
      }
      return fcont(dstBenv, c.l.userLattice.add(i, dstPos), store, c);
    }
    // END HELPERS
    
    return store;
  }
  
  function eval(state, c)
  {
    assertDefinedNotNull(state.benva);
    var tasks = [new Task("eval", function () {return evaluator.evalNode(state.node, state.stack, state.benva, state.store, state.time, c)})];
    return taskRunner(tasks);
  }
  
  function inject(o)
  {
    return new State(o.node, o.stack || [], o.benva || globala, o.store || store0, o.time || time0);
  }
  
  function context()
  {
    return { l:lattice,
      v:visited, 
      a:ag, 
      k:k, 
      e:evaluator, 
      OBJECTPA:OBJECTPA, 
      GLOBALA:GLOBALA, 
      createObject:createObject, 
      createClosure:createClosure, 
      createEnvironment:createEnvironment, 
      createArray:createArray,
      createString:createString}
  }
  
  function evalExit(state, c)
  {
    var result = [];
    
    var exitCont = new Cont("exit", state.node, null, globala,
    function (stack, store, time, c)
    {
      result = result.addLast(new State(null, stack, null, store, time)); 
      return [];
    });
    
    var initial = new State(state.node, state.stack.addFirst(exitCont), state.benva, state.store, state.time); 
    eval(initial, c);
    return result;
  }
  
  function evalNode(node)
  {
    var state = inject({node:node});
    var c = context();
    return evalExit(state, c);
  }
  
  
  function toString()
  {
    return "JIPDA [performGc " + performGc + " k " + k + " primLattice " + userLattice + " ag " + ag + " visited " + visited + " benvFactory " + benvFactory + "]";
  }
    	
  var store0 = new Store();
  store0 = createGlobal(store0);
	var time0 = new Time();	
  return {lattice:lattice, globalObject:globala, globalStore: store0, eval:eval, evalExit: evalExit, inject:inject, context:context, evalNode:evalNode, toString:toString};
}

// repls should move to instances
function repl(config)
{
  config = config || {};
  var lat = config.lat || new Lattice1();
  var visited = config.visited;
  var k = config.k || 0;
  var ag = config.ag || tagAg;
  var name = config.name || "jipda";
  var gc = config.gc === undefined ? true : config.gc;
  var jipda = new Jipda({k:k, lattice:lat, ag: ag, visited: visited, gc:gc});
  var c = jipda.context();
  var result = [jipda.inject({stack:[lat.abst1("I am Jipda!")]})];
  while (true)
  {
      var store = BOT;
      result.forEach(
          function (state, i)
          {
            var printer = new ConcretePrinter(lat, state.store);
            print(i + ":\t" + (state.stack[0].accept ? state.stack[0].accept(printer) : state.stack[0]));
            store = store.join(state.store);
          });
      write(name + "> ");
      var src = readline();
      if (":q".equals(src))
      {
        print("Bye!");
        break;
      }
      var state = jipda.inject({node:createAst(src), store:store});
      try
      {
        result = jipda.evalExit(state, c);
      }
      catch (e)
      {
        print(e);
        print(e.stack);
      }
  }
}

function concRepl(config)
{
  config = config || {};
  var concreteVisited = {};
  concreteVisited.visited = function (node, stack, benva, store, time) { return {store:store, stack:stack} };
  return repl({name: "conc", lat:new CpLattice(), visited:concreteVisited, ag:concreteAg, k:config.k});
}

function State(node, stack, benva, store, time)
{
  this.node = node;
  this.stack = stack;
  this.benva = benva;
  this.store = store;
  this.time = time;
}

State.store = function (state) {return state.store};
State.stack = function (state) {return state.stack};
State.topOfStack = function (state) {return state.stack[0]};

State.prototype.subsumes =
  function (x)
  {
    if (this.node !== x.node)
    {
      return false;
    }
    if (!Eq.equals(this.benva, x.benva))
    {
      return false;
    }
    if (!Eq.equals(this.time, x.time))
    {
      return false;
    }
    if (!this.store.subsumes(x.store))
    {
      return false;
    }
    var stack = this.stack;
    var contextStack = x.stack;
    for ( var si = 0; si < stack.length; si++)
    {
      if (stack[si] instanceof Cont)
      {
        break;
      }
    }
    var growth = stack.length - contextStack.length;
    if (growth >= 0)
    {
      var contextStackRoot = contextStack.slice(si);
      var stackRoot = stack.slice(si + growth);
      if (!stackSubsumes(stackRoot, contextStackRoot))
      {
        return false;
      }
//        var contextStackSi = contextStack.slice(0, si);
//        var stackSi = stack.slice(0, si);
//        if (stackSubsumes(stackSi, contextStackSi))
//        {
        var stackAdded = stack.slice(si, si + growth);
        var contextStackExisting = contextStack.slice(si, si + growth);
        return stackSubsumes(stackAdded, contextStackExisting);
//        }
    }
    return false;
  }
    
    
